T:Type. subtype_rel(T; )  (x:T, L:(T List). sorted(L)  sorted(s-insert(x; L))) 

latex

Definitions

type List, t  T, s = t, Type, x:AB(x), sorted(L), s-insert(x; l), P  Q, x:A. B(x), , l[i], int_seg(i; j), A  B, A, False, lelt(i; j; k), P  Q, ||as||, listp(A), cons(car; cdr), if b then t else f fi , i <z j, (i = j), l_all(L; T; x.P(x)), a < b, void, x. t(x), x:A  B(x), P  Q, P  Q, prop{i:l}, ff, , i z j, b, b, True, tt, T, eq_atom(x; y), null(as), set_blt(p; a; b), f(a), x f y, grp_blt(g; a; b), dcdr-to-bool(d), bimplies(p; q), band(p; q), bor(p; q), Unit, left + right, x.A(x), (x  l), guard(T), P  Q

Lemmas

member-s-insert, implies functionality wrt iff, l member wf, l all cons, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, not wf, eqtt to assert, assert of lt int, iff transitivity, eqff to assert, iff wf, rev implies wf, squash wf, true wf, bnot of lt int, assert of le int, lt int wf, bool wf, le int wf, assert wf, bnot wf, sorted-cons, l all wf, ifthenelse wf, length wf2, select wf, le wf, int seg wf, length wf1, subtype rel wf, s-insert wf, sorted wf